g:IMonoid, e:|g|. 0 x(*;e) e = e  |g| 

latex

Up	groups 1
Definitions of Statement	IMonoid, n x(op;id) e
Definitions	t  T, x:A. B(x), n x(op;id) e, P & Q, x. t(x), P  Q, P  Q, P  Q, IMonoid, x(s)
Lemmas	imon wf, grp car wf, grp id wf, int seg wf, itop unroll base